$\forall$$e$@$i$. $P$($e$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$e$:E. loc($e$) $=$ $i$ $\Rightarrow$ $P$($e$)